D:Dsys, l:IdLnk, tg:Id, T:Type. interface-check(D;l;tg;T)  Prop 

latex

Definitions	Prop, Id, IdLnk, Dsys, interface-check(D;l;tg;T), M.din(l,tg), M(i), destination(l), x:A. B(x), t  T
Lemmas	ldst wf, d-m wf, ma-din wf, subtype rel wf, dsys wf, IdLnk wf, Id wf